STM: ma-Msg wf

ABS: MsgA

STM: msga wf

ABS: ds(M)

STM: ma ds wf

ABS: da(M)

STM: ma da wf

ABS: M.ds(x)

STM: ma-ds wf

ABS: M.da(a)

ABS: a declared in M

STM: ma-decla wf

ABS: rcv(l,tg) declared in M

STM: ma-declm wf

STM: ma-da wf

ABS: M.din(l,tg)

STM: ma-din wf

ABS: M.dout(l,tg)

STM: ma-dout wf

ABS: M.init(x,v)

STM: ma-init wf

ABS: M.init(x)?v

STM: ma-init-val wf

ABS: M.state

STM: ma-st wf

ABS: M.Msg

STM: ma-msg wf

ABS: M.V(k)

STM: ma-v wf

ABS: unsolvable M.pre(a,s)

STM: ma-npre wf

ABS: M.pre(a,s,v)

STM: ma-pre wf

ABS: a in dom(M.pre)

STM: ma-has-pre wf

STM: decidable ma-has-pre

ABS: M.ef(k,x,s,v,w)

STM: ma-ef wf

ABS: M.ef(k,x,s,v)?w

STM: ma-ef-val wf

ABS: M.send(k;l;s;v;ms;i)

STM: ma-send wf

ABS: M.sends(k,s,v)

STM: ma-send-val wf

ABS: M sends on link l

STM: ma-sends-on wf

ABS: M.dout2(l;tg)

STM: ma-dout2 wf

ABS: M.frame(k affects x)

STM: ma-frame wf

ABS: M.sframe(k sends <l,tg>)

STM: ma-sframe wf

ABS: M.aframe(k affects x)

STM: ma-aframe wf

ABS: M.bframe(k sends on l)

STM: ma-bframe wf

ABS: M.rframe(k reads x)

STM: ma-rframe wf

ABS: M:k may not read x

STM: ma-no-read wf

STM: assert-ma-no-read

ABS: (s1  s2 mod x)

STM: ma-x-equiv wf

ABS: M.rframe(A.pre p for a)

ABS: M.rframe(A.effect f of k on y)

ABS: M.rframe(A.sends tfL of k on l)

ABS: M1  M2

STM: ma-sub wf

STM: ma-sub weakening

ABS: mk-ma

STM: mk-ma wf

ABS: 

STM: ma-empty wf

ABS: M1 ||decl M2

ABS: M1  M2

STM: ma-join wf

STM: ma-join-sends-on

STM: ma-sub-join-left

ABS: M1 || M2

STM: ma-compatible wf

STM: ma-compatible-symmetry

STM: ma-compatible-self

STM: ma-sub-join-right

STM: ma-empty-compatible-left

STM: ma-empty-compatible-right

ABS: x : t initially x = v

STM: ma-single-init wf

ABS: only members of L affect x :t

STM: ma-single-frame wf

ABS: only L sends on (l with tg)

STM: ma-single-sframe wf

ABS: k affects only members of L

STM: ma-single-aframe wf

ABS: k sends only on links in L

STM: ma-single-bframe wf

ABS: only members of L read x

STM: ma-single-rframe wf

ABS: with declarations ds:dsda:daeffect of k(v) is x := f s v

STM: ma-single-effect wf

ABS: with declarations ds:dsda:dak(v) sends f s v on link l

STM: ma-single-sends wf

ABS: (with ds: ds action a:T precondition a(v) is P s v)

STM: ma-single-pre wf

ABS: ma-frame-compat(A;B)

STM: ma-frame-compat wf

STM: ma-join-frame-compat

STM: ma-join-frame-compat2

ABS: ma-frame-compatible(A;B)

STM: ma-frame-compatible wf

ABS: Feasible(M)

STM: ma-feasible wf

STM: ma-feasible-ma-no-read

STM: ma-feasible-rframe-ef

STM: ma-feasible-rframe-send

STM: ma-empty-feasible

STM: ma-frame-compatible symmetry

STM: ma-empty-frame-compatible-left

STM: ma-empty-frame-compatible-right

STM: ma-join-compatible

ABS: A ||+ B

STM: ma-compat wf

STM: ma-compat-symmetry

STM: ma-compat weakening

STM: ma-empty-compat-left

STM: ma-empty-compat-right

STM: ma-join-feasible

STM: ma-compat-join

STM: ma-compat-join2

STM: ma-send-send-val

STM: ma-send-val-nil

STM: ma-send-val-nil2

STM: ma-feasible-bframe

STM: w-withlnk wf ma

STM: atom-free-ma-ds

STM: atom-free-ma-da

STM: atom-free-ma-dout